R-frame-compat(A; B)
== if Reffect?(A)
== ifthen if Rframe?(B)
== ifthen ifthen (Rframe-x(B) = Reffect-x(A))  (Reffect-knd(A)  Rframe-L(B))
== ifthen if Raframe?(B)
== ifthen ifthen (Raframe-k(B) = Reffect-knd(A))  (Reffect-x(A)  Raframe-L(B))
== ifthen if Rrframe?(B)
== ifthen ifthen (fpf-dom(id-deq; Rrframe-x(B); Reffect-ds(A)))  (Reffect-knd(A)  Rrframe-L(B))
== ifthen else True
== ifthen fi 
== if Rsends?(A)
== ifthen if Rsframe?(B)
== ifthen ifthen (Rsframe-lnk(B) = Rsends-l(A))
== ifthen ifthen  (Rsframe-tag(B)  map((p.p.1); Rsends-g(A)))
== ifthen ifthen  (Rsends-knd(A)  Rsframe-L(B))
== ifthen if Rbframe?(B)
== ifthen ifthen (Rbframe-k(B) = Rsends-knd(A))  (Rsends-l(A)  Rbframe-L(B))
== ifthen if Rrframe?(B)
== ifthen ifthen (fpf-dom(id-deq; Rrframe-x(B); Rsends-ds(A)))  (Rsends-knd(A)  Rrframe-L(B))
== ifthen else True
== ifthen fi 
== if Rpre?(A)
== ifthen if Rrframe?(B)
== ifthen then (fpf-dom(id-deq; Rrframe-x(B); Rpre-ds(A)))  (locl(Rpre-a(A))  Rrframe-L(B))
== ifthen else True
== ifthen fi 
== else True
== fi  

latex

---

clarification:

R-frame-compat(A; B)
== if Reffect?(A)
== ifthen if Rframe?(B)
== ifthen ifthen (Rframe-x(B) = Reffect-x(A)  Id)  (Reffect-knd(A)  Rframe-L(B)  Knd)
== ifthen if Raframe?(B)
== ifthen ifthen (Raframe-k(B) = Reffect-knd(A)  Knd)  (Reffect-x(A)  Raframe-L(B)  Id)
== ifthen if Rrframe?(B)
== ifthen ifthen (fpf-dom(id-deq; Rrframe-x(B); Reffect-ds(A)))
== ifthen ifthen  (Reffect-knd(A)  Rrframe-L(B)  Knd)
== ifthen else True
== ifthen fi 
== if Rsends?(A)
== ifthen if Rsframe?(B)
== ifthen ifthen (Rsframe-lnk(B) = Rsends-l(A)  IdLnk)
== ifthen ifthen  (Rsframe-tag(B)  map((p.p.1); Rsends-g(A))  Id)
== ifthen ifthen  (Rsends-knd(A)  Rsframe-L(B)  Knd)
== ifthen if Rbframe?(B)
== ifthen ifthen (Rbframe-k(B) = Rsends-knd(A)  Knd)  (Rsends-l(A)  Rbframe-L(B)  IdLnk)
== ifthen if Rrframe?(B)
== ifthen ifthen (fpf-dom(id-deq; Rrframe-x(B); Rsends-ds(A)))
== ifthen ifthen  (Rsends-knd(A)  Rrframe-L(B)  Knd)
== ifthen else True
== ifthen fi 
== if Rpre?(A)
== ifthen if Rrframe?(B)
== ifthen then (fpf-dom(id-deq; Rrframe-x(B); Rpre-ds(A)))
== ifthen then  (locl(Rpre-a(A))  Rrframe-L(B)  Knd)
== ifthen else True
== ifthen fi 
== else True
== fi  

latex

Definitions

True, Knd, Rrframe-L(x1), Rpre-a(x1), locl(a), (x  l), Rpre-ds(x1), Rrframe-x(x1), id-deq, fpf-dom(eq; x; f), b, P  Q, Rrframe?(x1), if b then t else f fi , Rpre?(x1), Rsends-knd(x1), Rsends-ds(x1), IdLnk, Rbframe-L(x1), Rsends-l(x1), Rbframe-k(x1), s = t, Rbframe?(x1), Rsframe-L(x1), Id, Rsends-g(x1), t.1, x.A(x), map(f; as), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Reffect-knd(x1), Reffect-ds(x1), Raframe-L(x1), Reffect-x(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1)

FDL editor aliases

R-frame-compat